import Yices

-- Some constants
jobs  = [1..12]
equip = [4..10]
endT  = 36

-- Declare the start-time array
s' :: Ident (Nat -> Nat)
(s',s) = ident1 "s"

-- The main script
main = printScript
    -- Declare the variable
    [ define s'
    -- The jobs must fit between 0 and endT
    , assert $ conj [nat 0 <= s i /\ (s i + nat i) <= nat endT | i <- jobs]
    -- Dependencies must be satisfied
    , assert $ deps
        [ (3, [1,2]), (5, [3,4]), (7, [3,4,6])
        , (9, [5,8]), (11, [10]), (12, [9,11])
        ]
    -- No more than two critical jobs simultaneously
    , assert $ conj [critJobs t <= nat 2 | t <- [0..endT-1]]
    ]
  where
    critJobs t = foldr ((+) . bool) (nat 0) [nat t >= s p /\ nat t < (s p + nat p) | p <- equip]
    deps   = conj . map (\(job, prereq) -> conj [s job >= (s p + nat p) | p <- prereq])
    bool x = ifte' ! x ! nat 1 ! nat 0
    x < y  = lt' ! x ! y
    x >= y  = ge' ! x ! y
    x <= y  = le' ! x ! y
    x + y  = plus' ! x ! y
    ifte' :: Ident (Bool -> Nat -> Nat -> Nat)
    ifte' = ident "if"
